From e134b6f156268364d3027e73910c19e9c7e09838 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 31 Jan 2007 18:36:04 +0000 Subject: [PATCH] Several bugs fixed: 1. mutual definitions were not generated correctly (e.g. let rec even ... and odd in even actually resulted in a definition of odd!) 2. a top-level mutual definition now generates two constants (as it should have always been) --- components/acic_content/cicNotationPp.ml | 3 + components/cic/cic.ml | 1 + components/cic/cicParser.ml | 1 + components/cic_acic/cic2Xml.ml | 2 + components/cic_disambiguation/disambiguate.ml | 68 ++++++++----------- components/grafite_parser/grafiteParser.ml | 15 +++- components/library/librarySync.ml | 42 ++++++++++++ 7 files changed, 91 insertions(+), 41 deletions(-) diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index 6d70c22c9..2873912c0 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -263,6 +263,7 @@ let pp_params pp_term = function let pp_flavour = function | `Definition -> "definition" + | `MutualDefinition -> assert false | `Fact -> "fact" | `Goal -> "goal" | `Lemma -> "lemma" @@ -301,6 +302,8 @@ let pp_obj pp_term = function (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) + | Ast.Theorem (`MutualDefinition, name, typ, body) -> + sprintf "<>" | Ast.Theorem (flavour, name, typ, body) -> sprintf "%s %s:\n %s\n%s" (pp_flavour flavour) diff --git a/components/cic/cic.ml b/components/cic/cic.ml index c5a5c1e40..1b02df3f1 100644 --- a/components/cic/cic.ml +++ b/components/cic/cic.ml @@ -57,6 +57,7 @@ type name = type object_flavour = [ `Definition + | `MutualDefinition | `Fact | `Lemma | `Remark diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml index 3122affd4..49a5a1ab7 100644 --- a/components/cic/cicParser.ml +++ b/components/cic/cicParser.ml @@ -667,6 +667,7 @@ let end_element ctxt tag = push ctxt (match pop_tag_attrs ctxt with | [ "value", "definition"] -> Obj_flavour `Definition + | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition | [ "value", "fact"] -> Obj_flavour `Fact | [ "value", "lemma"] -> Obj_flavour `Lemma | [ "value", "remark"] -> Obj_flavour `Remark diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml index afe22d374..c90bc348c 100644 --- a/components/cic_acic/cic2Xml.ml +++ b/components/cic_acic/cic2Xml.ml @@ -294,6 +294,8 @@ let xml_of_attrs attributes = in let flavour_of = function | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"] + | `MutualDefinition -> + Xml.xml_empty "flavour" [None, "value", "mutual_definition"] | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"] | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"] | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"] diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 1d4a6a61e..5c198cb59 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -86,7 +86,7 @@ let uniq_domain dom = in snd (aux [] dom) -let debug = false +let debug = true let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* @@ -267,14 +267,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast let cic_body = let unlocalized_body = aux ~localize:false loc context' body in match unlocalized_body with - Cic.Rel 1 -> `AvoidLetInNoAppl - | Cic.Appl (Cic.Rel 1::l) -> + Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n + | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> (try let l' = List.map (function t -> let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] 1 t + CicMetaSubst.delift_rels [] [] (List.length defs) t in assert (subst=[]); assert (metasenv=[]); @@ -286,10 +286,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast match body with CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn l' + `AvoidLetIn (n,l') | _ -> assert false else - `AvoidLetIn l' + `AvoidLetIn (n,l') with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> if localize then @@ -324,42 +324,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast (name, decr_idx, cic_type, cic_body)) defs in - let counter = ref ~-1 in - let build_term funs = - (* this is the body of the fold_right function below. Rationale: Fix - * and CoFix cases differs only in an additional index in the - * inductiveFun list, see Cic.term *) - match kind with - | `Inductive -> - (fun (var, _, _, _) cic -> - incr counter; - let fix = Cic.Fix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, fix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term fix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t))) + let fix_or_cofix n = + match kind with + `Inductive -> Cic.Fix (n,inductiveFuns) | `CoInductive -> - let funs = - List.map (fun (name, _, typ, body) -> (name, typ, body)) funs + let coinductiveFuns = + List.map + (fun (name, _, typ, body) -> name, typ, body) + inductiveFuns in - (fun (var, _, _, _) cic -> - incr counter; - let cofix = Cic.CoFix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, cofix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term cofix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t))) + Cic.CoFix (n,coinductiveFuns) in - (match - List.fold_right (build_term inductiveFuns) inductiveFuns - (`Recipe cic_body) - with - `Recipe _ -> assert false - | `Term t -> t) + let counter = ref ~-1 in + let build_term funs (var,_,_,_) t = + incr counter; + Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t) + in + (match cic_body with + `AvoidLetInNoAppl n -> + let n' = List.length inductiveFuns - n in + fix_or_cofix n' + | `AvoidLetIn (n,l) -> + let n' = List.length inductiveFuns - n in + Cic.Appl (fix_or_cofix n'::l) + | `AddLetIn cic_body -> + List.fold_right (build_term inductiveFuns) inductiveFuns + cic_body) | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed | CicNotationPt.Ident (name, subst) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 2d3789221..9a0cc9f43 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -574,6 +574,11 @@ EXTEND GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> + (* In case of mutual definitions here we produce just + the syntax tree for the first one. The others will be + generated from the completely specified term just before + insertion in the environment. We use the flavour + `MutualDefinition to rememer this. *) let name,ty = match defs with | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> @@ -588,8 +593,14 @@ EXTEND | _ -> assert false in let body = Ast.Ident (name,None) in - GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty, - Some (Ast.LetRec (ind_kind, defs, body)))) + let flavour = + if List.length defs = 1 then + `Definition + else + `MutualDefinition + in + GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index a4908ce7c..086893a97 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -405,12 +405,54 @@ let generate_inversion refinement_toolkit uri obj = add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri) (!build_inversion_principle uri obj) +let + generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid += + function + Cic.Fix (_,funs) -> + snd ( + List.fold_right + (fun (name,idx,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.Fix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | Cic.CoFix (_,funs) -> + snd ( + List.fold_right + (fun (name,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.CoFix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | _ -> assert false + let add_obj refinement_toolkit uri obj = add_single_obj uri obj refinement_toolkit; let uris = ref [] in try begin match obj with + | Cic.Constant (name,Some bo,_,_,attrs) when + List.mem (`Flavour `MutualDefinition) attrs -> + uris := + !uris @ + generate_sibling_mutual_definitions refinement_toolkit uri attrs + name bo | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ -- 2.39.2