added MkImplicit module for meta handling

diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend
index d22689dce5db9382b3a49b7707d61df544a71e03..0e37b8030904a57cbffac4d17cf838b585b7e304 100644 (file)
--- a/helm/ocaml/cic_unification/.depend
+++ b/helm/ocaml/cic_unification/.depend
@@ -3,3 +3,5 @@ cicUnification.cmo: cicUnification.cmi
 cicUnification.cmx: cicUnification.cmi 
 cicRefine.cmo: cicUnification.cmi cicRefine.cmi 
 cicRefine.cmx: cicUnification.cmx cicRefine.cmi 
+cicMkImplicit.cmo: cicMkImplicit.cmi 
+cicMkImplicit.cmx: cicMkImplicit.cmi 

diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile
index fbf0d22ed0929e374d0a7277d69e746c302089dd..1ce66e68d44bbc8d00519d182d9540a6bfd1e736 100644 (file)
--- a/helm/ocaml/cic_unification/Makefile
+++ b/helm/ocaml/cic_unification/Makefile
@@ -2,7 +2,7 @@ PACKAGE = cic_unification
 REQUIRES = helm-cic_proof_checking
 PREDICATES =
 
-INTERFACE_FILES = cicUnification.mli cicRefine.mli
+INTERFACE_FILES = cicMkImplicit.ml cicUnification.mli cicRefine.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
new file mode 100644 (file)
index 0000000..24a9451
--- /dev/null
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -0,0 +1,198 @@
+
+(* identity_relocation_list_for_metavariable i canonical_context         *)
+(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+(* where n = List.length [canonical_context]                             *)
+(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
+let identity_relocation_list_for_metavariable canonical_context =
+ let canonical_context_length = List.length canonical_context in
+  let rec aux =
+   function
+      (_,[]) -> []
+    | (n,None::tl) -> None::(aux ((n+1),tl))
+    | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
+  in
+   aux (1,canonical_context)
+
+(* Returns the first meta whose number is above the *)
+(* number of the higher meta.                       *)
+let new_meta metasenv =
+  let rec aux =
+   function
+      None,[] -> 1
+    | Some n,[] -> n
+    | None,(n,_,_)::tl -> aux (Some n,tl)
+    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+  in
+   1 + aux (None,metasenv)
+
+let mk_implicit metasenv context =
+  let newmeta = new_meta metasenv in
+  let irl = identity_relocation_list_for_metavariable context in
+  ([ newmeta, context, Cic.Sort Cic.Type ;
+    newmeta + 1, context, Cic.Meta (newmeta, irl);
+    newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv,
+   newmeta + 2)
+
+let mk_implicit' metasenv context =
+  let (metasenv, index) = mk_implicit metasenv context in
+  (metasenv, index - 1, index)
+
+let mk_implicit_type metasenv context =
+  let newmeta = new_meta metasenv in
+  let irl = identity_relocation_list_for_metavariable context in
+  ([ newmeta, context, Cic.Sort Cic.Type ;
+    newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
+   newmeta + 1)
+
+let expand_implicits metasenv context term =
+  let rec aux metasenv context = function
+    | (Cic.Rel _) as t -> metasenv, t
+    | (Cic.Sort _) as t -> metasenv, t
+    | Cic.Const (uri, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.Const (uri, subst')
+    | Cic.Var (uri, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.Var (uri, subst')
+    | Cic.MutInd (uri, i, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.MutInd (uri, i, subst')
+    | Cic.MutConstruct (uri, i, j, subst) ->
+        let metasenv', subst' = do_subst metasenv context subst in
+        metasenv', Cic.MutConstruct (uri, i, j, subst')
+    | Cic.Meta (n,l) -> 
+        let metasenv', l' = do_local_context metasenv context l in
+        metasenv', Cic.Meta (n, l')
+    | Cic.Implicit ->
+        let (metasenv', type_index, _) = mk_implicit' metasenv context in
+        let irl = identity_relocation_list_for_metavariable context in
+        metasenv', Cic.Meta (type_index, irl)
+    | Cic.Cast (te, ty) ->
+        let metasenv', ty' = aux metasenv context ty in
+        let metasenv'', te' = aux metasenv' context te in
+        metasenv'', Cic.Cast (te', ty')
+    | Cic.Prod (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        let metasenv'', t' =
+          aux metasenv' (Some (name, Cic.Decl s') :: context) t
+        in
+        metasenv'', Cic.Prod (name, s', t')
+    | Cic.Lambda (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        let metasenv'', t' =
+          aux metasenv' (Some (name, Cic.Decl s') :: context) t
+        in
+        metasenv'', Cic.Lambda (name, s', t')
+    | Cic.LetIn (name, s, t) ->
+        let metasenv', s' = aux metasenv context s in
+        let metasenv'', t' =
+          aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t
+        in
+        metasenv'', Cic.LetIn (name, s', t')
+    | Cic.Appl l when List.length l > 1 ->
+        let metasenv', l' =
+          List.fold_right
+            (fun term (metasenv, terms) ->
+              let new_metasenv, term = aux metasenv context term in
+              new_metasenv, term :: terms)
+            l (metasenv, [])
+        in
+        metasenv', Cic.Appl l'
+    | Cic.Appl _ -> assert false
+    | Cic.MutCase (uri, i, outtype, term, patterns) ->
+        let metasenv', l' =
+          List.fold_right
+            (fun term (metasenv, terms) ->
+              let new_metasenv, term = aux metasenv context term in
+              new_metasenv, term :: terms)
+            (outtype :: term :: patterns) (metasenv, [])
+        in
+        let outtype', term', patterns' =
+          match l' with
+          | outtype' :: term' :: patterns' -> outtype', term', patterns'
+          | _ -> assert false
+        in
+        metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
+    | Cic.Fix (i, funs) ->
+        let metasenv', types =
+          List.fold_right
+            (fun (name, _, typ, _) (metasenv, types) ->
+              let new_metasenv, new_type = aux metasenv context typ in
+              (new_metasenv, (name, new_type) :: types))
+            funs (metasenv, [])
+        in
+        let context' =
+          (List.rev_map
+            (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
+            types)
+          @ context
+        in
+        let metasenv'', bodies =
+          List.fold_right
+            (fun (_, _, _, body) (metasenv, bodies) ->
+              let new_metasenv, new_body = aux metasenv context' body in
+              (new_metasenv, new_body :: bodies))
+            funs (metasenv', [])
+        in
+        let rec combine = function
+          | ((name, index, _, _) :: funs_tl),
+            ((_, typ) :: typ_tl),
+            (body :: body_tl) ->
+              (name, index, typ, term) :: combine (funs_tl, typ_tl, body_tl)
+          | [], [], [] -> []
+          | _ -> assert false
+        in
+        let funs' = combine (funs, types, bodies) in
+        metasenv'', Cic.Fix (i, funs')
+    | Cic.CoFix (i, funs) ->
+        let metasenv', types =
+          List.fold_right
+            (fun (name, typ, _) (metasenv, types) ->
+              let new_metasenv, new_type = aux metasenv context typ in
+              (new_metasenv, (name, new_type) :: types))
+            funs (metasenv, [])
+        in
+        let context' =
+          (List.rev_map
+            (fun (name, t) -> Some (Cic.Name name, Cic.Decl t))
+            types)
+          @ context
+        in
+        let metasenv'', bodies =
+          List.fold_right
+            (fun (_, _, body) (metasenv, bodies) ->
+              let new_metasenv, new_body = aux metasenv context' body in
+              (new_metasenv, new_body :: bodies))
+            funs (metasenv', [])
+        in
+        let rec combine = function
+          | ((name, _, _) :: funs_tl),
+            ((_, typ) :: typ_tl),
+            (body :: body_tl) ->
+              (name, typ, term) :: combine (funs_tl, typ_tl, body_tl)
+          | [], [], [] -> []
+          | _ -> assert false
+        in
+        let funs' = combine (funs, types, bodies) in
+        metasenv'', Cic.CoFix (i, funs')
+  and do_subst metasenv context subst =
+    List.fold_right
+      (fun (uri, term) (metasenv, substs) ->
+        let metasenv', term' = aux metasenv context term in
+        (metasenv', (uri, term') :: substs))
+      subst (metasenv, [])
+  and do_local_context metasenv context local_context =
+    List.fold_right
+      (fun term (metasenv, local_context) ->
+        let metasenv', term' =
+          match term with
+          | None -> metasenv, None
+          | Some term ->
+              let metasenv', term' = aux metasenv context term in
+              metasenv', Some term'
+        in
+        metasenv', term' :: local_context)
+      local_context (metasenv, [])
+  in
+  aux metasenv context term
+

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli
new file mode 100644 (file)
index 0000000..919027b
--- /dev/null
+++ b/helm/ocaml/cic_unification/cicMkImplicit.mli
@@ -0,0 +1,27 @@
+
+(* identity_relocation_list_for_metavariable i canonical_context         *)
+(* returns the identity relocation list, which is the list               *)
+(* [Rel 1 ; ... ; Rel n] where n = List.length [canonical_context]       *)
+val identity_relocation_list_for_metavariable :
+  'a option list -> Cic.term option list
+
+(* Returns the first meta whose number is above the *)
+(* number of the higher meta.                       *)
+val new_meta : Cic.metasenv -> int
+
+(** [mk_implicit metasenv context]
+ * add a fresh metavariable to the given metasenv, using given context
+ * @return the new metasenv and the index of the added conjecture *)
+val mk_implicit: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+
+(** as above but return both the index of the added conjecture (2nd index) and
+ * the index of its type (1st index) *)
+val mk_implicit': Cic.metasenv -> Cic.context -> Cic.metasenv * int * int
+
+(** as above, but the fresh metavariable represents a type *)
+val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+
+val expand_implicits:
+  Cic.metasenv -> Cic.context -> Cic.term ->
+    Cic.metasenv * Cic.term
+