changed ast representation of exists

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 933397067539628cda6783a576879ff0ec362dab..45ff3d23306e8131883eaf5a0ce13f97e55a41db 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -78,7 +78,7 @@ let make_action action bindings =
     function
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 5 BEGIN *)
+    (* LUCA: DEFCON 4 BEGIN *)
     | Binding (name, Env.TermType) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
@@ -101,7 +101,7 @@ let make_action action bindings =
             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
     | Env _ :: tl ->
         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 5 END *)
+    (* LUCA: DEFCON 4 END *)
   in
     aux [] (List.rev bindings)
 
@@ -271,6 +271,13 @@ let fold_cluster binder terms ty body =
     (fun term body -> Ast.Binder (binder, (term, ty), body))
     terms body  (* terms are names: either Ident or FreshVar *)
 
+let fold_exists terms ty body =
+  List.fold_right
+    (fun term body ->
+      let lambda = Ast.Binder (`Lambda, (term, ty), body) in
+      Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+    terms body
+
 let fold_binder binder pt_names body =
   List.fold_right
     (fun (names, ty) body -> fold_cluster binder names ty body)
@@ -452,7 +459,7 @@ EXTEND
   ];
   binder: [
     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
-    | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+(*     | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
@@ -475,7 +482,8 @@ EXTEND
     | blob = UNPARSED_META ->
         let meta = !parse_level2_meta_ref (Stream.of_string blob) in
         match meta with
-        | Ast.Variable (Ast.FreshVar _) -> meta
+        | Ast.Variable (Ast.FreshVar _)
+        | Ast.Variable (Ast.IdentVar _) -> meta
         | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
         | _ -> failwith "Invalid index name."
     ]
@@ -548,6 +556,9 @@ EXTEND
     [
       [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           return_term loc (fold_cluster b vars typ body)
+      | SYMBOL <:unicode<exists>> (* ∃ *);
+        (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          return_term loc (fold_exists vars typ body)
       ]
     ];
   term: LEVEL "70L"  (* apply *)