spacepaste

Paste details

reply | raw

  1.  
  2. let encodeExpr ev e = bracket (match e with
  3. | Ident x -> (escape x)
  4. | EqOp (ex1,ex2) -> encodeExpr ev ex1^" = "^encodeExpr ev ex2
  5. | And (ex1,ex2) -> encodeExpr ev ex1^" "^wedge^" "^encodeExpr ev ex2
  6. | Or (ex1,ex2) -> encodeExpr ev ex1^" "^vee^" "^encodeExpr ev ex2
  7. | Not ex -> neg^" "^encodeExpr ev ex
  8. | Iff (ex1,ex2) -> encodeExpr ev ex1^" "^harr^" "^encodeExpr ev ex2
  9. | Implies (ex1,ex2) -> encodeExpr ev ex1^" "^rarr^" "^encodeExpr ev ex2
  10. | BFalse -> "False"
  11. | BTrue -> "True"
  12. | Appl app ->
  13. let (exf,ex) = getGenApp app in
  14. encodeExpr ev exf^" "^encodeExpr ev ex
  15. | Binder (q,VarSpec (vl,ty),ex) ->
  16. let qs = match q with
  17. | Forall -> " "^forall^" "
  18. | Exists -> " "^exists^" "
  19. | ExistsUniq -> " "^exists^"! "
  20. | Abs -> " "^lambda^" " in
  21. let (tys, ev') = match ty with
  22. | Some ty -> (" : "^encodeType ev ty, fold_left (fun e i -> addDecl e i ty) ev vl)
  23. | None -> ("",ev) in
  24. qs^(String.concat " , " (map escape vl))^tys^" . "^encodeExpr ev' ex
  25. | Desc (q,i,ty,ex) ->
  26. let qs = match q with
  27. | Iota -> " "^iota^" "
  28. | Epsilon -> " "^epsilon^" "
  29. in qs^i^" : "^encodeType ev ty^" . "^encodeExpr ev ex
  30. | Tuple exl ->
  31. fold_right
  32. (fun ex rest -> lang^" "^encodeExpr ev ex^" , "^ rest^" "^rang)
  33. exl
  34. (lang^rang)
  35. | If (ex1,ex2,ex3) -> "if "^encodeExpr ev ex1^" then "^encodeExpr ev ex2^ " else "^encodeExpr ev ex3
  36. | ConstrSel (ty, lbl) -> begin match normalize ev ty with
  37. | TInduct (id, fsl) ->
  38. let ctr = inductiveContainer id fsl in
  39. let (lam, bod) = findConstructor lbl ctr
  40. in lam^"roll "^bracket (inductiveContainerType ctr)^" "^bracket (bod)
  41. | _ -> raise (MatitaEncodeException "encodeExpr: No inductive type in constructor selector")
  42. end
  43. | Case (Ident id,cases) -> begin match cases with
  44. | [Branch (PatTuple pl, bdy)] ->
  45. let getIdent = function
  46. | PatIdent id -> id
  47. | PatNone | PatApp _ | PatTuple _ | PatRecord _ ->
  48. raise (MatitaEncodeException ("encodeExpr: complex patterns not supported"))
  49. in
  50. bracket
  51. (fold_right
  52. (fun i rest -> "'uncurry "^bracket(lambda^" "^escape i^" ."^rest))
  53. (List.map getIdent pl)
  54. ("'point "^encodeExpr ev bdy))
  55. ^ bracket (encodeExpr ev (Ident id))
  56. | _ ->
  57. match normalize ev
  58. (try
  59. (Util.StringMap.find id ev.tydecl)
  60. with Not_found ->
  61. raise (MatitaEncodeException ("encodeExpr: cannot find type for case analysis on "^id)))
  62. with
  63. | TInduct (ind, fsl) ->
  64. let ctr = inductiveContainer ind fsl in
  65. let pred = "P_"^ind in
  66. let return f = " return "^lambda^"w. ("^pred^" "^f "w"^" "^rarr^" "^pred^" s) "^rarr^" ? " in
  67. let header bdy = "let "^pred^" "^defeq^" pos "^bracket (inductiveContainerType ctr)^" in "
  68. ^ "match "^encodeExpr ev (Ident id)^" with "
  69. ^ "[roll r "^rArr^" match r with [contain s f "^rArr^" "^bdy
  70. ^ " ("^lambda^"x.x)]]" in
  71. let mkCase (lbl,cont) rest (bv,f) =
  72. let rec findLabel = function
  73. | PatIdent x -> x = lbl
  74. | PatApp (l,_) -> findLabel l
  75. | PatNone | PatTuple _ | PatRecord _ -> false
  76. in
  77. let Branch (p,bdy) = match List.filter (fun (Branch (p,_)) -> findLabel p) cases with
  78. | [] -> failwith ("encodeExpr: case "^lbl^" not found")
  79. | [p0] -> p0
  80. | _ -> failwith ("encodeExpr: multiple case "^lbl^" found") in
  81. let mkBranch _ rest (n,f) =
  82. let v = "z"^string_of_int n in
  83. let f' x = f (lang^v^", "^x^rang) in
  84. "match y"^return f^"with [pair "^v^" y "^rArr^" "^rest (n+1,f')^"]" in
  85. let rec content n = if 0 = n then sigma^"1 z" else sigma^"2"^bracket (content (n-1)) in
  86. let rec binds n p cont = match p, cont with
  87. | PatIdent _, [] -> ""
  88. | PatApp (p, PatIdent bv), c::cs ->
  89. "let "^escape bv^" "^defeq^" "^c.psi^" "^bracket ("contain ? ? z"^string_of_int n^" "^bracket (lambda^"z. f "^bracket ("cast "^bracket (content n))))^" in "^binds (n+1) p cs
  90. | _ -> raise (MatitaEncodeException ("encodeExpr: complex patterns not supported for inductive types"))
  91. in
  92. let endBranch (_,f) = "match y"^return f^"with [neo "^rArr^" "^lambda^"cast. "^binds 0 p cont^" "^encodeExpr ev bdy^"]" in
  93. "match "^bv^return f^"with "
  94. ^ "[ sigma1 y "^rArr^" "^fold_right mkBranch cont endBranch (0,fun x -> f (bracket (sigma^"1 "^x)))^" "
  95. ^ "| sigma2 x "^rArr^" "^rest ("x",fun x -> f (bracket (sigma^"2 "^x)))
  96. ^ "]" in
  97. let bdy = fold_right mkCase ctr (fun (bv,_) -> "[]"^bv) in
  98. header (bdy ("s",fun x -> x))
  99. | _ -> failwith ("encodeExpr: not an inductive type for "^id)
  100. end
  101. | _ ->
  102. let module M = Printers.Make(Printers.Configuration.ASCII)(Printers.Options.StdOpt)
  103. (struct let f = Format.str_formatter end) in
  104. let _ = M.expr e in
  105. raise (MatitaEncodeException ("encodeExpr: not implemented:"^Format.flush_str_formatter ()))
  106. )
  107.  
Powered by spacepaste. Paste removal.