X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;h=a3cdfbb78603d3237e3006fc5ecfb41543a279e5;hb=2f73b29c0ae7e4f0fa77934db55ebf811638fce3;hp=81e94419699624d13c167accbe0b8bccff80f3e7;hpb=7e60b896247a228beea1b2a547c1f606e1834921;p=helm.git diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 81e944196..a3cdfbb78 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -23,21 +23,26 @@ * http://cs.unibo.it/helm/. *) -exception NotImplemented;; - type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; +let gen_id seed = + let res = "i" ^ string_of_int !seed in + incr seed ; + res +;; + let fresh_id seed ids_to_terms ids_to_father_ids = fun father t -> - let res = "i" ^ string_of_int !seed in - incr seed ; + let res = gen_id seed in Hashtbl.add ids_to_father_ids res father ; Hashtbl.add ids_to_terms res t ; res ;; +let source_id_of_id id = "#source#" ^ id;; + exception NotEnoughElements;; exception NameExpected;; @@ -52,7 +57,7 @@ let rec get_nth l n = ;; let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context t expectedty + ids_to_inner_types metasenv context idrefs t expectedty = let module D = DoubleTypeInference in let module T = CicTypeChecker in @@ -61,7 +66,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let terms_to_types = D.double_type_of metasenv context t expectedty in - let rec aux computeinnertypes father context tt = + let rec aux computeinnertypes father context idrefs tt = let fresh_id'' = fresh_id' father tt in (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) let aux' = aux computeinnertypes (Some fresh_id'') in @@ -70,14 +75,14 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (*CSC: This is a very inefficient way of computing inner types *) (*CSC: and inner sorts: very deep terms have their types/sorts *) (*CSC: computed again and again. *) - let string_of_sort = - function + let string_of_sort t = + match CicReduction.whd context t with C.Sort C.Prop -> "Prop" | C.Sort C.Set -> "Set" | C.Sort C.Type -> "Type" | _ -> assert false in - let ainnertypes,innertype,innersort = + let ainnertypes,innertype,innersort,expected_available = (*CSC: Here we need the algorithm for Coscoy's double type-inference *) (*CSC: (expected type + inferred type). Just for now we use the usual *) (*CSC: type-inference, but the result is very poor. As a very weak *) @@ -94,21 +99,25 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts D.expected = None} in let innersort = T.type_of_aux' metasenv context synthesized in - let ainnertypes = + let ainnertypes,expected_available = if computeinnertypes then - Some - {annsynthesized = - aux false (Some fresh_id'') context synthesized ; - annexpected = + let annexpected,expected_available = match expected with - None -> None + None -> None,false | Some expectedty' -> - Some (aux false (Some fresh_id'') context expectedty') - } + Some + (aux false (Some fresh_id'') context idrefs expectedty'), + true + in + Some + {annsynthesized = + aux false (Some fresh_id'') context idrefs synthesized ; + annexpected = annexpected + }, expected_available else - None + None,false in - ainnertypes, synthesized, string_of_sort innersort + ainnertypes,synthesized, string_of_sort innersort, expected_available in let add_inner_type id = match ainnertypes with @@ -123,70 +132,125 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | _ -> raise NameExpected in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.ARel (fresh_id'', n, id) - | C.Var uri -> + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + C.ARel (fresh_id'', List.nth idrefs (n-1), n, id) + | C.Var (uri,exp_named_subst) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AVar (fresh_id'', uri) + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AVar (fresh_id'', uri,exp_named_subst') | C.Meta (n,l) -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv + in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; C.AMeta (fresh_id'', n, - (List.map - (function None -> None | Some t -> Some (aux' context t)) l)) + (List.map2 + (fun ct t -> + match (ct, t) with + | None, _ -> None + | _, Some t -> Some (aux' context idrefs t) + | Some _, None -> assert false (* due to typing rules *)) + canonical_context l)) | C.Sort s -> C.ASort (fresh_id'', s) | C.Implicit -> C.AImplicit (fresh_id'') | C.Cast (v,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; - C.ACast (fresh_id'', aux' context v, aux' context t) + C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t) | C.Prod (n,s,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' (string_of_sort innertype) ; - C.AProd - (fresh_id'', n, aux' context s, - aux' ((Some (n, C.Decl s))::context) t) + let sourcetype = T.type_of_aux' metasenv context s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + let n' = + match n with + C.Anonymous -> n + | C.Name n' -> + if D.does_not_occur 1 t then + C.Anonymous + else + C.Name n' + in + C.AProd + (fresh_id'', n', aux' context idrefs s, + aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t) | C.Lambda (n,s,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - begin - let father_is_lambda = - match father with - None -> false - | Some father' -> - match Hashtbl.find ids_to_terms father' with - C.Lambda _ -> true - | _ -> false - in - if not father_is_lambda then - add_inner_type fresh_id'' - end ; - C.ALambda - (fresh_id'',n, aux' context s, - aux' ((Some (n, C.Decl s)::context)) t) + let sourcetype = T.type_of_aux' metasenv context s in + Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') + (string_of_sort sourcetype) ; + if innersort = "Prop" then + begin + let father_is_lambda = + match father with + None -> false + | Some father' -> + match Hashtbl.find ids_to_terms father' with + C.Lambda _ -> true + | _ -> false + in + if (not father_is_lambda) || expected_available then + add_inner_type fresh_id'' + end ; + C.ALambda + (fresh_id'',n, aux' context idrefs s, + aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) | C.LetIn (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.ALetIn - (fresh_id'', n, aux' context s, - aux' ((Some (n, C.Def s))::context) t) + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ALetIn + (fresh_id'', n, aux' context idrefs s, + aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t) | C.Appl l -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; - C.AAppl (fresh_id'', List.map (aux' context) l) - | C.Const (uri,cn) -> + C.AAppl (fresh_id'', List.map (aux' context idrefs) l) + | C.Const (uri,exp_named_subst) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AConst (fresh_id'', uri, cn) - | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) - | C.MutConstruct (uri,cn,tyno,consno) -> + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AConst (fresh_id'', uri, exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AMutInd (fresh_id'', uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) - | C.MutCase (uri, cn, tyno, outty, term, patterns) -> + if innersort = "Prop" && expected_available then + add_inner_type fresh_id'' ; + let exp_named_subst' = + List.map + (function i,t -> i, (aux' context idrefs t)) exp_named_subst + in + C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then add_inner_type fresh_id'' ; - C.AMutCase (fresh_id'', uri, cn, tyno, aux' context outty, - aux' context term, List.map (aux' context) patterns) + C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty, + aux' context idrefs term, List.map (aux' context idrefs) patterns) | C.Fix (funno, funs) -> + let fresh_idrefs = + List.map (function _ -> gen_id seed) funs in + let new_idrefs = List.rev fresh_idrefs @ idrefs in let tys = List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs in @@ -194,12 +258,16 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts if innersort = "Prop" then add_inner_type fresh_id'' ; C.AFix (fresh_id'', funno, - List.map - (fun (name, indidx, ty, bo) -> - (name, indidx, aux' context ty, aux' (tys@context) bo) - ) funs + List.map2 + (fun id (name, indidx, ty, bo) -> + (id, name, indidx, aux' context idrefs ty, + aux' (tys@context) new_idrefs bo) + ) fresh_idrefs funs ) | C.CoFix (funno, funs) -> + let fresh_idrefs = + List.map (function _ -> gen_id seed) funs in + let new_idrefs = List.rev fresh_idrefs @ idrefs in let tys = List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs in @@ -207,23 +275,24 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts if innersort = "Prop" then add_inner_type fresh_id'' ; C.ACoFix (fresh_id'', funno, - List.map - (fun (name, ty, bo) -> - (name, aux' context ty, aux' (tys@context) bo) - ) funs + List.map2 + (fun id (name, ty, bo) -> + (id, name, aux' context idrefs ty, + aux' (tys@context) new_idrefs bo) + ) fresh_idrefs funs ) in - aux true None context t + aux true None context idrefs t ;; -let acic_of_cic_context metasenv context t = +let acic_of_cic_context metasenv context idrefs t = let ids_to_terms = Hashtbl.create 503 in let ids_to_father_ids = Hashtbl.create 503 in let ids_to_inner_sorts = Hashtbl.create 503 in let ids_to_inner_types = Hashtbl.create 503 in let seed = ref 0 in acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context t, + ids_to_inner_types metasenv context idrefs t, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; @@ -241,55 +310,98 @@ let acic_object_of_cic_object obj = let acic_term_of_cic_term_context' = acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types in - let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] in + let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in let aobj = match obj with - C.Definition (id,bo,ty,params) -> + C.Constant (id,Some bo,ty,params) -> let abo = acic_term_of_cic_term' bo (Some ty) in let aty = acic_term_of_cic_term' ty None in - C.ADefinition ("mettereaposto",id,abo,aty,(Cic.Actual params)) - | C.Axiom (id,ty,params) -> raise NotImplemented - | C.Variable (id,bo,ty) -> raise NotImplemented - | C.CurrentProof (id,conjectures,bo,ty) -> + C.AConstant + ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params) + | C.Constant (id,None,ty,params) -> + let aty = acic_term_of_cic_term' ty None in + C.AConstant + ("mettereaposto",None,id,None,aty, params) + | C.Variable (id,bo,ty,params) -> + let abo = + match bo with + None -> None + | Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) + in + let aty = acic_term_of_cic_term' ty None in + C.AVariable + ("mettereaposto",id,abo,aty, params) + | C.CurrentProof (id,conjectures,bo,ty,params) -> let aconjectures = List.map (function (i,canonical_context,term) as conjecture -> let cid = "c" ^ string_of_int !conjectures_seed in Hashtbl.add ids_to_conjectures cid conjecture ; incr conjectures_seed ; - let acanonical_context = - let rec aux = + let idrefs',revacanonical_context = + let rec aux context idrefs = function - [] -> [] + [] -> idrefs,[] | hyp::tl -> let hid = "h" ^ string_of_int !hypotheses_seed in + let new_idrefs = hid::idrefs in Hashtbl.add ids_to_hypotheses hid hyp ; incr hypotheses_seed ; match hyp with (Some (n,C.Decl t)) -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl in let at = - acic_term_of_cic_term_context' conjectures tl t None + acic_term_of_cic_term_context' + conjectures context idrefs t None in - (hid,Some (n,C.ADecl at))::(aux tl) + final_idrefs,(hid,Some (n,C.ADecl at))::atl | (Some (n,C.Def t)) -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl in let at = - acic_term_of_cic_term_context' conjectures tl t None + acic_term_of_cic_term_context' + conjectures context idrefs t None in - (hid,Some (n,C.ADef at))::(aux tl) - | None -> (hid,None)::(aux tl) + final_idrefs,(hid,Some (n,C.ADef at))::atl + | None -> + let final_idrefs,atl = + aux (hyp::context) new_idrefs tl + in + final_idrefs,(hid,None)::atl in - aux canonical_context + aux [] [] (List.rev canonical_context) in let aterm = - acic_term_of_cic_term_context' conjectures canonical_context - term None + acic_term_of_cic_term_context' conjectures + canonical_context idrefs' term None in - (cid,i,acanonical_context,aterm) + (cid,i,(List.rev revacanonical_context),aterm) ) conjectures in - let abo = acic_term_of_cic_term_context' conjectures [] bo (Some ty) in - let aty = acic_term_of_cic_term_context' conjectures [] ty None in - C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty) - | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented + let abo = + acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in + let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in + C.ACurrentProof + ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) + | C.InductiveDefinition (tys,params,paramsno) -> + let context = + List.map + (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in + let idrefs = List.map (function _ -> gen_id seed) tys in + let atys = + List.map2 + (fun id (name,inductive,ty,cons) -> + let acons = + List.map + (function (name,ty) -> + (name, + acic_term_of_cic_term_context' [] context idrefs ty None) + ) cons + in + (id,name,inductive,acic_term_of_cic_term' ty None,acons) + ) (List.rev idrefs) tys + in + C.AInductiveDefinition ("mettereaposto",atys,params,paramsno) in aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, ids_to_conjectures,ids_to_hypotheses